Problem:
a__f(f(X)) -> a__c(f(g(f(X))))
a__c(X) -> d(X)
a__h(X) -> a__c(d(X))
mark(f(X)) -> a__f(mark(X))
mark(c(X)) -> a__c(X)
mark(h(X)) -> a__h(mark(X))
mark(g(X)) -> g(X)
mark(d(X)) -> d(X)
a__f(X) -> f(X)
a__c(X) -> c(X)
a__h(X) -> h(X)
Proof:
Bounds Processor:
bound: 3
enrichment: match
automaton:
final states: {9,8,7,6}
transitions:
h1(172) -> 173*
h1(174) -> 175*
h1(164) -> 165*
h1(166) -> 167*
h1(180) -> 181*
c1(142) -> 143*
c1(156) -> 157*
c1(158) -> 159*
c1(148) -> 149*
c1(150) -> 151*
f1(20) -> 21*
f1(15) -> 16*
f1(17) -> 18*
f1(34) -> 35*
f1(26) -> 27*
f1(28) -> 29*
d1(50) -> 51*
d1(52) -> 53*
d1(42) -> 43*
d1(44) -> 45*
d1(36) -> 37*
g1(132) -> 133*
g1(134) -> 135*
g1(124) -> 125*
g1(126) -> 127*
g1(16) -> 17*
g1(140) -> 141*
a__h1(118) -> 119*
mark1(92) -> 93*
mark1(94) -> 95*
mark1(84) -> 85*
mark1(86) -> 87*
mark1(76) -> 77*
a__c1(60) -> 61*
a__c1(102) -> 103*
a__c1(74) -> 75*
a__c1(116) -> 117*
a__c1(66) -> 67*
a__c1(108) -> 109*
a__c1(68) -> 69*
a__c1(58) -> 59*
a__c1(18) -> 19*
a__c1(110) -> 111*
a__c1(100) -> 101*
a__f1(77) -> 78*
h2(280) -> 281*
a__f0(5) -> 6*
a__f0(2) -> 6*
a__f0(4) -> 6*
a__f0(1) -> 6*
a__f0(3) -> 6*
c2(262) -> 263*
c2(254) -> 255*
c2(234) -> 235*
c2(276) -> 277*
c2(256) -> 257*
c2(246) -> 247*
c2(268) -> 269*
c2(248) -> 249*
c2(238) -> 239*
c2(270) -> 271*
c2(240) -> 241*
f0(5) -> 1*
f0(2) -> 1*
f0(4) -> 1*
f0(1) -> 1*
f0(3) -> 1*
f2(232) -> 233*
f2(283) -> 284*
a__c0(5) -> 7*
a__c0(2) -> 7*
a__c0(4) -> 7*
a__c0(1) -> 7*
a__c0(3) -> 7*
a__c2(227) -> 228*
g0(5) -> 2*
g0(2) -> 2*
g0(4) -> 2*
g0(1) -> 2*
g0(3) -> 2*
d2(212) -> 213*
d2(182) -> 183*
d2(224) -> 225*
d2(204) -> 205*
d2(226) -> 227*
d2(206) -> 207*
d2(196) -> 197*
d2(218) -> 219*
d2(198) -> 199*
d2(188) -> 189*
d2(220) -> 221*
d2(190) -> 191*
d0(5) -> 3*
d0(2) -> 3*
d0(4) -> 3*
d0(1) -> 3*
d0(3) -> 3*
c3(292) -> 293*
a__h0(5) -> 8*
a__h0(2) -> 8*
a__h0(4) -> 8*
a__h0(1) -> 8*
a__h0(3) -> 8*
d3(287) -> 288*
mark0(5) -> 9*
mark0(2) -> 9*
mark0(4) -> 9*
mark0(1) -> 9*
mark0(3) -> 9*
g2(282) -> 283*
c0(5) -> 4*
c0(2) -> 4*
c0(4) -> 4*
c0(1) -> 4*
c0(3) -> 4*
h0(5) -> 5*
h0(2) -> 5*
h0(4) -> 5*
h0(1) -> 5*
h0(3) -> 5*
1 -> 166,148,134,110,92,42,28
2 -> 174,156,126,102,84,50,20
3 -> 164,142,140,116,94,36,34
4 -> 172,150,132,108,86,44,26
5 -> 180,158,124,100,76,52,15
16 -> 6*
18 -> 248,198
19 -> 6*
21 -> 6,16
27 -> 6,16
29 -> 6,16
35 -> 6,16
37 -> 95,77,118,9,58,7
43 -> 95,77,118,9,60,7
45 -> 95,77,118,9,66,7
51 -> 95,77,118,9,68,7
53 -> 95,77,118,9,74,7
58 -> 246,196
59 -> 8*
60 -> 276,224
61 -> 8*
66 -> 268,218
67 -> 8*
68 -> 262,212
69 -> 8*
74 -> 270,220
75 -> 8*
77 -> 232,118
78 -> 93,77,118,9
85 -> 77*
87 -> 77*
93 -> 77*
95 -> 77*
100 -> 256,206
101 -> 87,77,118,9
102 -> 234,182
103 -> 87,77,118,9
108 -> 240,190
109 -> 87,77,118,9
110 -> 254,204
111 -> 87,77,118,9
116 -> 238,188
117 -> 87,77,118,9
118 -> 280,226
119 -> 77,118,9
125 -> 85,77,118,9
127 -> 85,77,118,9
133 -> 85,77,118,9
135 -> 85,77,118,9
141 -> 85,77,118,9
143 -> 7*
149 -> 7*
151 -> 7*
157 -> 7*
159 -> 7*
165 -> 8*
167 -> 8*
173 -> 8*
175 -> 8*
181 -> 8*
183 -> 103*
189 -> 117*
191 -> 109*
197 -> 59*
199 -> 19*
205 -> 111*
207 -> 101,9
213 -> 69,8
219 -> 67,8
221 -> 75,8
225 -> 61,8
227 -> 292,287
228 -> 78,93,119,9
233 -> 282,78,9
235 -> 103*
239 -> 117*
241 -> 109*
247 -> 59*
249 -> 19*
255 -> 111*
257 -> 101,9
263 -> 69,8
269 -> 67,8
271 -> 75,8
277 -> 61,8
281 -> 119,9
284 -> 227*
288 -> 228,119
293 -> 228,119
problem:
Qed